/* @LICENSE(NICTA_CORE) */

#include <sel4/bootinfo.h>

seL4_BootInfo* bootinfo;

void seL4_InitBootInfo(seL4_BootInfo* bi)
{
    bootinfo = bi;
}

seL4_BootInfo* seL4_GetBootInfo()
{
    return bootinfo;
}
